package mac5739;

import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import org.apache.commons.io.IOUtils;

import mac5739.experimento.SingleElementRemainderSetOperator;
import bcontractor.api.SATReasoner;
import bcontractor.api.SentenceSet;
import bcontractor.base.PureSentenceSet;
import bcontractor.partialmeet.PartialMeetContractionOperator;
import bcontractor.partialmeet.RemainderSetOperator;
import bcontractor.partialmeet.SelectionFunction;
import bcontractor.partialmeet.selection.FullSelectionFunction;
import bcontractor.propositional.PropositionalSentence;
import bcontractor.propositional.minisat.MiniSatInput;
import bcontractor.propositional.minisat.MiniSatReasoner;

/**
 * Programa a ser executado manualmente.
 * @author lundberg
 *
 */
public class Main {

	/**
	 * @param args
	 * @throws IOException IOException
	 */
	public static void main(String[] args) throws IOException {
		if(args == null || args.length != 3) {
			System.out.println("Modo de usar: java -jar projeto2.jar <arquivo com B, DIMACS> <arquivo com alpha, DIMACS> <arquivo de saída>");
			System.exit(1);
		}
		try {
			SentenceSet<PropositionalSentence> sentences = parseSentences(args[0]);
			PropositionalSentence sentence = parseSentence(args[1]);
			SentenceSet<PropositionalSentence> contracted = contract(sentences, sentence);
			renderOutput(contracted, args[2]);
			System.exit(0);
		} catch (RuntimeException e) {
			System.out.println(e.getMessage());
			System.exit(1);
		}
	}

	private static void renderOutput(SentenceSet<PropositionalSentence> contracted, String fileName) {
		File output = new File(fileName);
		if(output.exists()) {
			output.delete();
		}
		OutputStream stream = null;
		try {
			stream = new FileOutputStream(output);
			IOUtils.copy(new MiniSatInput(contracted), stream);
		} catch (IOException e) {
			throw new RuntimeException("Erro de I/O escrevendo saída: " + e.getMessage(), e);
		} finally {
			IOUtils.closeQuietly(stream);
		}
	}

	private static SentenceSet<PropositionalSentence> parseSentences(
			String fileName) {
		List<String> tokens = readFile(fileName);
		SentenceSet<PropositionalSentence> sentences = new PureSentenceSet<PropositionalSentence>();
		List<Integer> clauseBuffer = new ArrayList<Integer>();
		for(String token : tokens.subList(4, tokens.size())) {
			if("0".equals(token)) {
				int[] clause = new int[clauseBuffer.size()];
				for(int i = 0; i < clauseBuffer.size(); i++) {
					clause[i] = clauseBuffer.get(i);
				}
				clauseBuffer.clear();
				sentences = sentences.with(new PropositionalSentence(clause));
			} else {
				clauseBuffer.add(Integer.parseInt(token));
			}
		}
		return sentences;
	}

	private static List<String> readFile(String fileName) {
		InputStream input = null;
		try {
			input = new FileInputStream(fileName);
			return Arrays.asList(IOUtils.toString(input).split("\\s"));
		} catch (FileNotFoundException e) {
			throw new RuntimeException("Arquivo não encontrado:" + fileName, e);
		} catch (IOException e) {
			throw new RuntimeException("Erro de I/O lendo arquivo:" + e.getMessage(), e);
		} finally {
			IOUtils.closeQuietly(input);
		}
	}

	private static PropositionalSentence parseSentence(String fileName) {
		SentenceSet<PropositionalSentence> sentences = parseSentences(fileName);
		if(sentences.size() != 1) {
			throw new RuntimeException("O Alpha deve ter exatamente uma cláusula.");
		}
		return sentences.iterator().next();
	}

	private static SentenceSet<PropositionalSentence> contract(
			SentenceSet<PropositionalSentence> sentences,
			PropositionalSentence sentence) {
		SATReasoner<PropositionalSentence> reasoner = new MiniSatReasoner();
		RemainderSetOperator<PropositionalSentence> remainder = new SingleElementRemainderSetOperator<PropositionalSentence>(reasoner);
		SelectionFunction<PropositionalSentence> selection = new FullSelectionFunction<PropositionalSentence>();
		PartialMeetContractionOperator<PropositionalSentence> contraction = new PartialMeetContractionOperator<PropositionalSentence>(remainder, selection);
		return contraction.eval(sentences, sentence);
	}

}
